00100	
00200	REPRESENTATION OF THE MISSIONARIES AND CANNIBALS PROBLEM
00300	
00400	
00500		The problem  of  the  missionaries  and  cannibals  has  been
00600	treated  by Newell (196.) and by Amarel (196.).  Like Amarel, I shall
00700	be concerned with the representation of the problem in the memory  of
00800	a   problem   solving   program.   However,  he  evaluates  different
00900	representations according to the ease with which the problem  can  be
01000	solved  when  so formulated.  I shall be somewhat concerned with this
01100	problem but even more with trying  to  get  a  formulation  that  can
01200	accept  a  statement  of  the problem containing just the information
01300	available to a human who has to solve it.  I am  not  concerned  with
01400	understanding  English,  however,  and  will  use the language of set
01500	theory  to  express  this  information.  Besides  trying  to  get  an
01600	expression  of the statement of the problem, I am also concerned with
01700	formal expression of the general information available to a human who
01800	can  solve  the  problem.   Here,  the  goal  is to be fair - i.e. to
01900	express only general information that can  be  assumed  to  be  known
02000	before  the  problem  is  encountered in a way that is not especially
02100	adapted to the problem in advance.  It is further necessary to  point
02200	out that the problem may be taken in two ways - either as the problem
02300	faced by a man who is asked for advice by  a  group  of  missionaries
02400	faced by a river and some cannibals or as that faced by a man reading
02500	a puzzle.  The first man would be inclined to ask whether there was a
02600	bridge  and  the  second would rule out such a question as not in the
02700	spirit of the puzzle.
02800	
02900		We   shall   be   interested   in   the   problem   from  the
03000	epistemological point of view as discussed  in  (McCarthy  and  Hayes
03100	1969)  and not much interested in the heuristic problem which we want
03200	to postpone till we understand the  problem  epistemologically.   The
03300	reasons for this are discussed in that paper.
03400	
03500		For definiteness, we shall refer  to  the  following  English
03600	expression of the problem:
03700	
03800		"Three missionaries and three cannibals  travelling  together
03900	come  to a river which they want to cross.  There is a boat available
04000	that can hold two people and can be rowed by one.   However,  if  the
04100	cannibals  ever  outnumber  the  missionaries  on  either  bank,  the
04200	outnumbered missionaries will be eaten.  How can they all get  safely
04300	across?"
04400	
04500		The simplest  informal  mathematical  representation  of  the
04600	problem  is  to represent a state by a triplet (m,c,b) whose elements
04700	are the numbers of missionaries, cannibals, and boats respectively on
04800	the  starting bank of the river.  The initial state is represented by
04900	331 and the desired final state  by  000.   The  condition  to  avoid
05000	cannibalism is
05100	
05200		(m=0 ∨ m≥c) ∧ (m=3 ∨ m≤c)
05300	
05400	and the transformations corresponding to rowing are
05500	
05600	(m,c,b) → (m-2b+1,c,1-b),
05700	
05800	(m,c,b) → (m-4b+2,c,1-b),
05900	
06000	(m,c,b) → (m,c-2b+1,1-b),
06100	
06200	(m,c,b) → (m,c-4b+2,1-b),
06300	
06400	and
06500	
06600	(m,c,b) → (m-2b+1,c-2b+1,1-b).
06700	
06800	Every intermediate state must also satisfy the physical condition
06900	
07000		0≤m≤3 ∧ 0≤c≤3.
07100	
07200	In this formulation, the well known solution is
07300	
07400		331→310→321→300→311→110→221→020→031→010→021→000.
07500	
07600	Each state satisfies  both  the  non-cannibalism  condition  and  the
07700	physical condition, and each state except the initial one is obtained
07800	from the immediately preceding state  by  one  of  the  five  allowed
07900	transformations.
08000	
08100		In order to understand the motivation of  what  follows,  the
08200	reader  must  understand  why  we  are  not  satisfied with the above
08300	elegant  representation.   From  the  heuristic  point  of  view  the
08400	representation  is  just fine; the solution is found from the initial
08500	condition and the set of allowed transformations by  a  rather  small
08600	tree  search  which  corresponds  rather well to the tree search that
08700	most  humans  go  through  in  solving   the   problem.    From   the
08800	epistemological point of view, however, this mathematical formulation
08900	is not the problem but the solution.  The epistemological problem  is
09000	to go from the desire to cross the river and a knowledge of the facts
09100	to such a nice mathematical formulation.  In  this  paper,  we  shall
09200	discuss  only part of that problem, namely:  Give a formal expression
09300	of the particular facts that honestly represents what is known  about
09400	the  problem  (whether  it  be from reading the English or seeing the
09500	scene on the river bank);  also  give  a  formal  expression  of  the
09600	general  knowledge  that a human brings to bear on the problem (about
09700	rivers, boats, the effects of rowing, etc.).  This formal  expression
09800	must  be  adequate  in the sense that how to get the missionaries and
09900	cannibals across the river is a logical consequence of the expression
10000	of the two sets of facts.
10100	
10200		We shall not treat understanding the English or  the  problem
10300	of retrieving the relevant facts from memory or the heuristic part of
10400	going from the facts to the mathematical formulation.  The problem we
10500	have  set  ourselves  is quite hard enough, and, as you will see, the
10600	solutions given are not as honest as one would  like.   Namely,  they
10700	expression of general information is a bit too well suited to solving
10800	this particular problem, and the special information is  given  in  a
10900	form a bit too suited to the general method to be used.
11000	
11100		We  shall  give  several  formulations starting with one very
11200	close to the "result formalism" of (McCarthy and  Hayes  1969).   The
11300	later  formulations will avoid some of the defects we shall point out
11400	in the early ones.
11500	
11600		We shall use the notation of set  theory  imbedded  in  first
11700	order logic.  In particular, we need the membership relation, the set
11800	of individuals satisfying a predicate, the union of sets, the  notion
11900	of  the  cardinality  of  small finite sets, and enough arithmetic to
12000	calculate how many cannibals remain when two  cross  the  river.  The
12100	axioms of set theory to be used are given in Appendix A.
12200	
12300		FORMULATION I
12400	
12500		1. M denotes the set of missionaries and C denotes the set of
12600	cannibals,  the  boat  is called Boat, and the banks of the river are
12700	called LB and RB.  The initial situation is called S0.  We  have  the
12800	following facts labelled f1,f2, etc.:
12900	
13000	f1:	card M = 3
13100	f2:	card C = 3
13200	
13300	f3:	(∀x) x ε M∪C ⊃ at(x,LB,S0)
13400	
13500	f4:	at(Boat,LB,S0)
13600	
13700		2. Some general information about not objects  not  being  in
13800	two different places at once specializes in this case to
13900	
14000	f5:	(∀x s) ¬at(x,LB,s) ∨ ¬at(x,RB,s)
14100	
14200		3. We shall express our goal as that of proving the sentence
14300	
14400	goal:	(∃s) attainable(s) ∧ (∀x) x ε M∪C ⊃ at(x,RB,s)
14500	
14600	As we shall later see, this formulation is somewhat of a shortcut.
14700	Using it, however, we have the special fact
14800	
14900	f6:	attainable(S0)
15000	
15100	and the general fact about actions
15200	
15300	f7:	(∀s s' u) attainable(s) ∧ s' = result(u,s) ⊃ attainable(s')
15400	
15500	Here we have deviated from (McCarthy and Hayes 1969) in omitting  the
15600	person  argument from result.  In this case, it requires more thought
15700	before we can formulate who  does  what.   Are  the  missionaries  and
15800	cannibals  moved  like  chessmen  or do we have to make some argument
15900	about what they are respectively motivated to do.  Certainly, in  the
16000	puzzle  context,  their  motivation is not given much thought, but if
16100	you actually met them in the jungle, you might have  to  consider  it
16200	further.
16300	
16400		4. Now we have a small fact introducing an auxiliary
16500	function
16600	
16700	f8:	opp(LB) = RB ∧ opp(RB) = LB.
16800	
16900	It is used in the next axiom, but it is not important because it
17000	could be replaced there by a conditional expression.
17100	
17200		5. Now we give the effect of rowing:
17300	
17400	f9:	(∀s b r) safe(s) ∧ at(Boat,b,s) ∧ (card r = 1 ∨ card r = 2)
17500	
17600			∧ r ⊂ M∪C ∧ ((∀x) x ε r ⊃ at(x,b,s)
17700	
17800					⊃
17900	
18000		((λs') ((∀x) x ε M∪C ⊃ (if x ε r then at(x,opp(b),s') else
18100	
18200			at(x,b,s')) ∧ at(Boat,opp(b),s'))(result(row(r),s)).
18300	
18400	
18500		6. Finally, we express the fact that safety requires that the
18600	cannibals not outnumber the missionaries on either bank:
18700	
18800	f10:	(∀s) safe(s) ≡ (card {x|x ε M ∧ at(x,LB,s)} = 0
18900	
19000			∨ card {x | x ε M ∧ at(x,LB,s)} ≥
19100	
19200					card {x | x ε C ∧ at(x,LB,s)})
19300	
19400					∧
19500	
19600		(card {x | x ε M ∧ at(x,RB,s)} = 0
19700	
19800			∨ card {x | x ε M ∧ at(x,RB,s)} ≥
19900	
20000					card {x | x ε C ∧ at(x,RB,s)}).
20100	
20200	This statement has a lot of repetition  that  can  be  eliminated  by
20300	rather  fierce  use of the lambda notation or by the use of auxiliary
20400	functions.
20500	
20600		The most straightforward way of proving the  goal  attainable
20700	from  these  facts  will  be  quite long even if we take all relevant
20800	general theorems of set theory and arithmetic  without  proof.   This
20900	proof  will  follow  the  informal mathematical proof by successively
21000	proving the attainability of situations with  the  right  numbers  of
21100	missionaries,  cannibals,  and  boats  on the two banks of the river.
21200	Another approach is to prove a correspondence between a  mathematical
21300	formalization  using  triplets of numbers and the formalization given
21400	above.  Then a proof of the solvability of the  mathematical  problem
21500	will  transform  into  a  proof  of  the attainability of the desired
21600	situation.
21700	
21800		There is, however, an even stronger possibility.  Suppose  we
21900	have  a  logical  system  in which the result of a calculation can be
22000	asserted as an axiom, i.e. there is an axiom schema  of  calculation.
22100	The  calculations could be in LISP, for example.  This is reasonable,
22200	because when the result of a  calculation  was  asserted,  the  proof
22300	checker  could  just  carry  it out.  Then all we have to do is prove
22400	that the attainability of the  desired  situation  follows  from  the
22500	success  of  the usual tree search for the missionaries and cannibals
22600	problem.
22700	
22800	More about this in the next exciting installment.
22900	
23000	ADDITIONAL FORMALISM
23100	
23200	
23300		Here are some defects in the above formalism and some possible
23400	remedies.
23500	
23600		1. Rather than merely proving that there is an attainable
23700	situation that satisfies the goal condition,
23800	it would be better to prove
23900	that a certain strategy achieves the goal.  The difficulty is that if
24000	a strategy is to have a precise situation as a result it must somehow
24100	specify which missionary or cannibal goes across each time, but to do
24200	this would abandon one of the main advantages of the set theoretic
24300	formulation of the problem.  We can get around this by revising the
24400	formalism so that the result of an occurrence is a set of situations
24500	which has other advantages also.
24600	
24700		Then we shall want to prove.
24800	
24900	r1:	(∀s) s ε result(STRAT,S0) ⊃ ((∀x) x ε M∪C ⊃
25000	
25100			at(x,RB,s) ∧ alive(x,s)).
25200	
25300	Here STRAT denotes some expression representing a strategy.  (We are
25400	using all caps here for meta-variables.